A, B:Realizer. R-icompat(A;B)  R-icompat(B;A) 

latex

Definitions	True, P & Q, ff, tt, if b then t else f fi , , Y, R-icompat(A;B), i  j , False, A, A  B, t  T, P  Q, x:A. B(x), {T}, P  Q, P  Q, Unit, , , ,
Lemmas	not functionality wrt iff, assert-eq-id, R-interface-compat wf, Id wf, R-loc wf, eq id wf, true wf, Rnone? wf, R-size-decreases, Rplus-right wf, Rplus-left wf, R-icompat-Rplus2, Rplus-implies, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, not wf, bnot wf, assert wf, bool wf, Rplus? wf, ge wf, nat properties, le wf, es realizer wf, R-icompat wf, nat plus wf, R-size wf, nat wf